#include <stdio.h>

void prtnum( int num ) {
  printf( "%d\n", num ) ;
}

